COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	unique[f83,jmc]		The unique names assumption
C00006 ENDMK
C⊗;
unique[f83,jmc]		The unique names assumption

	Ray Reiter pointed out that the treatment proposed in
my letter to him didn't work.  Here's another try.

Suppose we want to conclude that Joe is different from Henry if
this is permitted by some knowledge A(Joe,Henry) that we are
taking into account.  We circumscribe the expression

	Joe = Henry

regarding Joe and Henry as variable - not taking
equality to be variable as previous
attempts tried to.  We get

A(Joe,Henry) ∧ ∀Joe' Henry'.A(Joe',Henry') ∧ (Joe' = Henry' ⊃ Joe = Henry)
		⊃ (Joe = Henry ≡ Joe' = Henry').

If the axioms A(Joe,Henery) permit Joe ≠ Henry,
 then we can take for Joe' and Henry'
distinct individuals satisfying A(Joe',Henry').  This makes the left
side of the inequality true, and so we can conclude

	Joe ≠ Henry.

This is a great simplification of our previous attempts, because
we don't have to bother with names as objects and denotation
as a function.  I'm reasonably convinced that it's the right
formalism, but there are some conceptual problems that need
additional thought.

	Perhaps A(Joe,Henry) should include ∃x y.x ≠ y or even
∃x y.person(x) ∧ person(y) ∧ x ≠ y.  This wouldn't suffice if
we had ten individuals and were expected to jump to the conclusion
that they are all distinct.  We would need a stronger axiom
asserting the existence of enough individuals of the desired
kind.

	This sort of works for inferring that two specific objects
are distinct if possible.  However, suppose we have a whole collection
of objects, and we want as many as possible to be distinct.  Extending
the above method to four objects gives a six way parallel circumscription
which is reducible to a single circumscription by Lifschitz's
trick - namely we circumscribe  E(x,z) defined by

	(z = 1 ∧ x1 = x2) ∨ (z = 2 ∧ x1 = x3) ∨ (z = 3 ∧ x2 = x3) ∨
(z = 4 ∧ x1 = x4) ∨ (z = 5 ∧ x2 = x4) ∨ (z = 6 ∧ x2 = x4)

as a predicate of z with x1, x2, . . . ,x6 variable.  We have

A(x1, ... ,x6) ∧ ∀x1' ... x6'.A(x1',...x6') ∧ (∀z.E(x',z) ⊃ E(x,z))
		⊃(∀z.E(x,z) ≡ E(x',z))